MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: cond_div_mod_n_m(Pair(0(),x2),x1) -> Triple(0(),x1,x2) cond_div_mod_n_m(Pair(S(x3),x2),x1) -> cond_div_mod_n_m_2(div_mod#2(S(x3),x2),x2) cond_div_mod_n_m_2(Triple(x4,x3,x2),x1) -> Triple(plus#2(S(0()),x4),x3,x1) cond_eval_e_1(Triple(x12,x13,x14)) -> x12 div_mod#2(x8,x4) -> cond_div_mod_n_m(Pair(minus'#2(x8,x4),x4),x8) eval#1(Eadd(x2,x1)) -> plus#2(eval#1(x2),eval#1(x1)) eval#1(Econst(x1)) -> x1 eval#1(Ediv(x2,x1)) -> eval_e_6#1(x2,eval#1(x1)) eval#1(Emult(x2,x1)) -> mult#2(eval#1(x2),eval#1(x1)) eval_e_6#1(x11,0()) -> ite_b#2(True(),cond_eval_e_1(div_mod#2(eval#1(x11),0()))) eval_e_6#1(x11,S(x24)) -> ite_b#2(False(),cond_eval_e_1(div_mod#2(eval#1(x11),S(x24)))) eval_e_6#1(x11,S(0())) -> ite_b#2(True(),cond_eval_e_1(div_mod#2(eval#1(x11),S(0())))) main(x28) -> eval#1(x28) minus'#2(0(),x24) -> 0() minus'#2(S(x28),0()) -> S(x28) minus'#2(S(x4),S(x2)) -> minus'#2(x4,x2) mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x16,0()) -> x16 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {cond_div_mod_n_m/2,cond_div_mod_n_m_2/2,cond_eval_e_1/1,div_mod#2/2,eval#1/1,eval_e_6#1/2,main/1,minus'#2/2 ,mult#2/2,plus#2/2} / {0/0,Eadd/2,Econst/1,Ediv/2,Emult/2,False/0,Pair/2,S/1,Triple/3,True/0,ite_b#2/2} - Obligation: innermost runtime complexity wrt. defined symbols {cond_div_mod_n_m,cond_div_mod_n_m_2,cond_eval_e_1 ,div_mod#2,eval#1,eval_e_6#1,main,minus'#2,mult#2,plus#2} and constructors {0,Eadd,Econst,Ediv,Emult,False ,Pair,S,Triple,True,ite_b#2} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE